|
In computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not expressed within the calculus. The concept of explicit substitutions has become notorious (despite a large number of published calculi of explicit substitutions in the literature with quite different characteristics) because the notion often turns up (implicitly and explicitly) in formal descriptions and implementation of all the mathematical forms of substitution involving variables such as in abstract machines, predicate logic, and symbolic computation. == Basics == A simple example of a lambda calculus with explicit substitution is "λx", which adds one new form of term to the lambda calculus, namely the form M⟨x:=N⟩, which reads "M where x will be substituted by N". (The meaning of the new term is the same as the common idiom let x:=N in M from many programming languages.) λx can be written with the following rewriting rules: # (λx.M) N → M⟨x:=N⟩ # x⟨x:=N⟩ → N # x⟨y:=N⟩ → x (x≠y) # (M1M2) ⟨x:=N⟩ → (M1⟨x:=N⟩) (M2⟨x:=N⟩) # (λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y) While making substitution explicit, this formulation still retains the complexity of the lambda calculus "variable convention", requiring arbitrary renaming of variables during reduction to ensure that the "(x≠y)" condition on the last rule is always satisfied before applying the rule. Therefore many calculi of explicit substitution avoid variable names altogether by using a so-called "name-free" De Bruijn index notation. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「explicit substitution」の詳細全文を読む スポンサード リンク
|